\section{On Interface Compatibility}\label{sec:int}
%In , we mentioned that 
The  reduction semantics of Sect.\ref{sec:syn} 
is parametric with respect to a compatibility relation $\compat$ on interfaces $\Delta$.
We now informally discuss some alternatives;  a  formal treatment of interface compatibility
is left for future work.

Until now,
%In our developments, 
we assumed $\compat \, \triangleq \, = $, therefore  
requiring that interfaces should be exactly the same.
%This is the definition we considered in the example of Sect.\ref{sec:exam}.
This definition may be overly restrictive in specifications.
A more flexible definition can be obtained by exploiting \emph{subtyping}. %,DBLP:conf/sac/BernardiH12}.
Given types $\rho, \sigma$, we say that 
$\rho$ is a \emph{subtype} of $\sigma$ (noted $\rho \leq \sigma$) 
if, 
intuitively, 
any process of type $\rho$ can safely be used in a context where a process of type $\sigma$ is expected. 
%``every value described by S is also described by T''-values of type $\rho$ can be safely used whenever values of type $\sigma$ are expected.
%is more general than $\rho$. 
Subtyping for session types
has been studied in~\cite{DBLP:journals/acta/GayH05,DBLP:journals/fuin/VallecilloVR06}; it 
arises from subset relations
on basic types (as in, e.g., $\mathsf{int} \leq \mathsf{real}$) and from branching and selection constructs.
Assuming $\rho_i \leq \sigma_i$, for all $i \in \{1, \ldots, m\}$ and $k \geq 0$, we have:
\begin{eqnarray*}
 \&\{n_1:\rho_1,\ldots, n_k:\rho_m \} & \leq & \&\{n_1:\sigma_1,\ldots, n_j:\sigma_{m+k} \} \\
\oplus\{n_1:\rho_1,\ldots, n_j:\rho_{m+k} \} & \leq &  \oplus\{n_1:\sigma_1,\ldots, n_k:\sigma_m \} 
\end{eqnarray*}
Moreover, $\leq$ is co-variant for input prefixes and contra-variant for outputs.
This way,
a compatibility relation based on $\leq$  %noted $\compat_s$, 
could be defined by means of a bijection $f{:}\Delta_1 \to \Delta_2$, 
such that for all $\rho \in \Delta_1$, we have $\rho \leq f(\rho)$.
%Furthermore, 
Another compatibility relation could rely on the \emph{type equivalence} induced by
$\leq$: % induces an equivalence on types:
types $\sigma$ and $\sigma'$
are equivalent if $\sigma \leq \sigma'$ and $\sigma' \leq \sigma$ hold.
(This can be formalized by adopting an equi-recursive convention for recursive types.)
Other definitions for $\compat$ could be obtained by enriching $\intf{P}$
with information on the \emph{distributed structure} (location nesting) in $P$. 
This would allow to combine structural and behavioral considerations when reasoning about interfaces.
In general, 
incorporating these definitions of compatibility 
%typing rules such as \rulename{t-Loc} and \rulename{t-Upd} 
would require (minor) adjustments in our type system (precisely, in rules such as \rulename{t:Loc} and \rulename{t:Upd}).
%Again, we leave the study of such alternative definitions for future work.